T:Type, as, bs, cs:T List. cs  as  (b:T. cs = (as @ (b.bs))  False) 

latex

Definitions	t  T, x:A. B(x), ij, ||as||, False, Top, S  T, AB, P  Q, l1  l2, as @ bs, Prop, P  Q, P & Q, P  Q
Lemmas	append wf, false wf, iseg wf, iseg length, le wf, length wf1, length-append, top wf, non neg length